Example 4.7.77 in [Borralleras - PhD'03]

Summary: Ex4_7_77_Bor03

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (Polynomials @ MuTerm)
  2. Ferreira and Ribeiro's transformation (Polynomials @ MuTerm)
  3. Giesl and Middeldorp's transformation (Polynomials @ MuTerm)
  4. CSKBO
  5. CSRPO
  6. Polynomial interpretation (MuTerm)
  7. CSDP

CS-TRS Ex4_7_77_Bor03 (file Ex4_7_77_Bor03.csr)

Functions:  zeros cons 0 tail

Constructors:  cons 0

Variables:  X XS

Arities: 

ar(zeros) = 0
ar(cons) = 2
ar(0) = 0
ar(tail) = 1

Replacement map: 

µ(zeros)={}
µ(cons)={1}
µ(0)={}
µ(tail)={1}

Rules: (file Ex4_7_77_Bor03) 

zeros -> cons(0,zeros)
tail(cons(X,XS)) -> XS

The CS-TRS in OBJ format (file Ex4_7_77_Bor03.obj):

obj Ex4_7_77_Bor03 is
  sort S .
  op zeros : -> S .
  op cons : S S -> S [strat (1 0)] .
  op 0 : -> S .
  op tail : S -> S .
  vars X XS : S .
  eq zeros = cons(0,zeros) .
  eq tail(cons(X,XS)) = XS .
endo

Negative results

1. The µ-termination of Ex4_7_77_Bor03 cannot be proved by using Lucas' transformation: The TRS Ex4_7_77_Bor03_L:

       zeros -> cons(0,zeros)
       tail(cons(X)) -> XS
       

   contains extra variables.

Positive results

1. The µ-termination of Ex4_7_77_Bor03 can be proved by using Zantema's transformation. The TRS Ex4_7_77_Bor03_Z:

       zeros -> cons(0,n__zeros)
       tail(cons(X,XS)) -> activate(XS)
       zeros -> n__zeros
       activate(n__zeros) -> zeros
       activate(X) -> X
       

   can be proved terminating by using a polynomial interpretation (use MuTerm).
2. The µ-termination of Ex4_7_77_Bor03 can also be proved by using Ferreira and Ribeiro's transformation. The TRS Ex4_7_77_Bor03_FR is the same that Ex4_7_77_Bor03_Z
3. The µ-termination of Ex4_7_77_Bor03 can also be proved by using Giesl and Middeldorp's transformation: the TRS Ex4_7_77_Bor03_GM:

       a__zeros -> cons(0,zeros)
       a__tail(cons(X,XS)) -> mark(XS)
       mark(zeros) -> a__zeros
       mark(tail(X)) -> a__tail(mark(X))
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(0) -> 0
       a__zeros -> zeros
       a__tail(X) -> tail(X)
       

   can be proved terminating by using a polynomial interpretation (use MuTerm).
4. The µ-termination of Ex4_7_77_Bor03 is proved in [Bor03, Example 4.7.77] by using CSKBO:
   • marking map:

           m(cons,2)={zeros}
           

   • Weight function:

            w(0)=w(_zeros)=2
            w(zeros)=6
            w(cons)=1
            w(tail)=2
            w0 = 2
           

5. The µ-termination of Ex4_7_77_Bor03 (since Ex4_7_77_Bor03 is a subset of Ex1_BLR02; see [BLR02, Example 10] for a proof based on CSRPO).Automatically can be proved by MuTerm :
6. The µ-termination of Ex4_7_77_Bor03 can also be proved by using a polynomial interpretation (computed with MuTerm):

       Proof of termination for CS-TRS  Ex4_7_77_Bor03:
   
       [zeros] = 1
       [cons](X1,X2) = X1 + 1/2.X2
       [0] = 0
       [tail](X) = 2.X + 1
       

7. The µ-termination of Ex4_7_77_Bor03 can also be proved by using CSDP (computed by MuTerm).